hasproperty(ctxm(dot,al,d_2,id_2,cd_2),ctxm(dot,al,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(kappa_,al,d_2,id_2,cd_2),ctxm(kappa_,al,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(pi_,u,d_2,id_2,cd_2),ctxm(pi_,u,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(zeta_,u,d_2,id_2,cd_2),ctxm(zeta_,u,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(xi_,u,d_2,id_2,cd_2),ctxm(xi_,u,d_4,id_4,cd_4),gt60).

knows(ttp,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(ttp,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(ttp,ctxm(dot,is,ip,ip_is,ip_is)).
knows(ttp,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(ttp,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(ttp,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(ttp,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(ttp,ctxm(dot,ttp,kM,kM_ttp,kM_ttp)).
knows(ttp,pri(pk,[ctxm(dot,ca,kM,kM_ca,kM_ca)])).
knows(ii,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(ii,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(ii,ctxm(dot,is,ip,ip_is,ip_is)).
knows(ii,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(ii,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(ii,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(ii,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(ii,ctxm(dot,ii,kM,kM_ii,kM_ii)).
knows(ii,ctxm(kappa_,al,i_ii,i_al_ii,i_al_ii)).
knows(ii,ctxm(kappa_,al,d_1,id_1,cd_1)).
knows(ii,ctxm(kappa_,al,d_2,id_2,cd_2)).
knows(ii,ctxm(kappa_,al,d_3,id_3,cd_3)).
knows(ii,ctxm(pi_,u,i_ii,i_al_ii,i_al_ii)).
knows(ii,pri(pk,[ctxm(dot,ca,kM,kM_ca,kM_ca)])).
knows(ii,pri(lst,[pri(lst,[ctxm(dot,ii,id,id_ii,id_ii),pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)]),ctxm(dot,dot,n_ii,in_ii,cn_ii)]),pri(sig,[pri(lst,[ctxm(dot,ii,id,id_ii,id_ii),pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)]),ctxm(dot,dot,n_ii,in_ii,cn_ii)]),ctxm(dot,ca,kM,kM_ca,kM_ca)])])).
knows(ii,ctxm(pi_,dot,n_b,ss(pi_,i_n_b),ss(pi_,c_n_b))).
knows(is,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(is,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(is,ctxm(dot,is,ip,ip_is,ip_is)).
knows(is,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(is,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(is,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(is,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(is,ctxm(dot,is,kM,kM_is,kM_is)).
knows(is,ctxm(mu_,al,i_is,i_al_is,i_al_is)).
knows(is,ctxm(mu_,al,d_5,id_5,cd_5)).
knows(is,ctxm(mu_,al,d_6,id_6,cd_6)).
knows(is,ctxm(eta_,u,i_is,i_al_is,i_al_is)).
knows(is,pri(pk,[ctxm(dot,ca,kM,kM_ca,kM_ca)])).
knows(is,pri(lst,[pri(lst,[ctxm(dot,is,id,id_is,id_is),pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)]),ctxm(dot,dot,n_is,in_is,cn_is)]),pri(sig,[pri(lst,[ctxm(dot,is,id,id_is,id_is),pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)]),ctxm(dot,dot,n_is,in_is,cn_is)]),ctxm(dot,ca,kM,kM_ca,kM_ca)])])).
knows(is,ctxm(eta_,dot,n_b,ss(eta_,i_n_b),ss(eta_,c_n_b))).
knows(bs,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(bs,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(bs,ctxm(dot,is,ip,ip_is,ip_is)).
knows(bs,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(bs,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(bs,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(bs,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(bs,ctxm(dot,bs,kM,kM_bs,kM_bs)).
knows(bs,ctxm(zeta_,u,d_7,id_71,cd_71)).
knows(bs,ctxm(xi_,u,d_7,id_72,cd_72)).
knows(bs,pri(pk,[ctxm(dot,ca,kM,kM_ca,kM_ca)])).
knows(bs,pri(lst,[pri(lst,[ctxm(dot,bs,id,id_bs,id_bs),pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)]),ctxm(dot,dot,n_bs,in_bs,cn_bs)]),pri(sig,[pri(lst,[ctxm(dot,bs,id,id_bs,id_bs),pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)]),ctxm(dot,dot,n_bs,in_bs,cn_bs)]),ctxm(dot,ca,kM,kM_ca,kM_ca)])])).
knows(bs,ctxm(zeta_,dot,n_b,ss(zeta_,i_n_b),ss(zeta_,c_n_b))).
knows(bs,ctxm(zeta_,dot,dm,ss(zeta_,i_dm),ss(zeta_,c_dm))).
knows(bs,ctxm(zeta_,dot,q,ss(zeta_,i_q),ss(zeta_,c_q))).
knows(bs,ctxm(xi_,dot,n_b,ss(xi_,i_n_b),ss(xi_,c_n_b))).
knows(bs,ctxm(xi_,dot,dm,ss(xi_,i_dm),ss(xi_,c_dm))).
knows(bs,ctxm(xi_,dot,q,ss(xi_,i_q),ss(xi_,c_q))).
knows(al,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(al,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(al,ctxm(dot,is,ip,ip_is,ip_is)).
knows(al,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(al,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(al,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(al,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(al,ctxm(dot,al,i,i_al,i_al)).
knows(al,ctxm(dot,al,i_ii,i_al_ii,i_al_ii)).
knows(al,ctxm(dot,al,i_is,i_al_is,i_al_is)).
knows(al,ctxm(dot,al,d_1,id_1,cd_1)).
knows(al,ctxm(dot,al,d_2,id_2,cd_2)).
knows(al,ctxm(dot,al,d_3,id_3,cd_3)).
knows(al,ctxm(dot,al,d_5,id_5,cd_5)).
knows(al,ctxm(dot,al,d_6,id_6,cd_6)).
knows(al,ctxm(pi_,u,i_ii,i_al_ii,i_al_ii)).
knows(al,ctxm(eta_,u,i_is,i_al_is,i_al_is)).
knows(al,ctxm(zeta_,u,i,i_al,i_al)).
knows(al,ctxm(xi_,u,i,i_al,i_al)).
knows(al,ctxm(pi_,u,ip,ip_al_1,ip_al_1)).
knows(al,ctxm(eta_,u,ip,ip_al_2,ip_al_2)).
knows(al,ctxm(zeta_,u,ip,ip_al_3,ip_al_3)).
knows(al,ctxm(xi_,u,ip,ip_al_4,ip_al_4)).
knows(al,pri(pk,[ctxm(dot,ca,kM,kM_ca,kM_ca)])).
knows(al,pri(lst,[pri(lst,[ctxm(dot,dot,id_c,iid_c,iid_c),pri(pk,[ctxm(dot,dot,kM_c,kM_c,kM_c)]),ctxm(dot,dot,n_c,in_c,cn_c)]),pri(sig,[pri(lst,[ctxm(dot,dot,id_c,iid_c,iid_c),pri(pk,[ctxm(dot,dot,kM_c,kM_c,kM_c)]),ctxm(dot,dot,n_c,in_c,cn_c)]),ctxm(dot,ca,kM,kM_ca,kM_ca)])])).
knows(al,ctxm(dot,dot,kM_c,kM_c,kM_c)).
knows(al,ctxm(dot,al,i,i_al,i_al)).
knows(al,ctxm(pi_,dot,n_a,ss(pi_,i_n_a),ss(pi_,c_n_a))).
knows(al,ctxm(eta_,dot,n_a,ss(eta_,i_n_a),ss(eta_,c_n_a))).
knows(al,ctxm(zeta_,dot,n_v,in_z_v,cn_z_v)).
knows(al,ctxm(zeta_,u,i_sess,ss(zeta_,i_sess),ss(zeta_,i_sess))).
knows(al,ctxm(zeta_,dot,n_a,ss(zeta_,i_n_a),ss(zeta_,c_n_a))).
knows(al,ctxm(xi_,dot,n_v,in_x_v,cn_x_v)).
knows(al,ctxm(xi_,u,i_sess,ss(xi_,i_sess),ss(xi_,i_sess))).
knows(al,ctxm(xi_,dot,n_a,ss(xi_,i_n_a),ss(xi_,c_n_a))).
